\begin{tabbing}
world{-}rename(${\it rx}$;${\it ra}$;${\it rt}$;${\it rainv}$;${\it rtinv}$;$w$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\langle$($\lambda$$i$,$x$. w{-}vartype($w$; $i$; (${\it rx}$($x$))))\+
\\[0ex]$,\,$($\lambda$$i$,$a$. 1of(2of($w$))($i$,${\it ra}$($a$)))
\\[0ex]$,\,$($\lambda$$l$,${\it tg}$. $w$.M($l$,${\it rt}$(${\it tg}$)))
\\[0ex]$,\,$($\lambda$$i$,$t$,$x$. w{-}s($w$; $i$; $t$; (${\it rx}$($x$))))
\\[0ex]$,\,$($\lambda$$i$,$t$. action{-}rename(${\it rainv}$;${\it rtinv}$;w{-}a($w$; $i$; $t$)))
\\[0ex]$,\,$($\lambda$$i$,$t$. mapfilter($\lambda$$m$.msg{-}rename(${\it rtinv}$;$m$);$\lambda$$m$.isl(${\it rtinv}$(mtag($m$)));w{-}m($w$; $i$; $t$)))
\\[0ex]$,\,$($\lambda$$i$.NullMachine)
\\[0ex]$,\,$$\cdot$$\rangle$
\-
\end{tabbing}